$\forall$$T$:Type, $n$:$\mathbb{N}$, $f$:(int\_seg(0; $n$)$\rightarrow$$T$), $i$:int\_seg(0; $n$). mklist($n$; $f$)[$i$] = $f$($i$)